es:ES, i:Id, L:IdLnk List, T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 (e:E. loc(e) = i  ||"table" when e||  = ||"table" when es-init(es;e)||   ) 

latex

Definitions	"$x", P  Q, Id, x. t(x), t  T, x:A. B(x), es-frame(es;i;L;x;T), Top, Prop, e@i. P(e), es-secret-server, P & Q, , @i only events in L change   x : T, A & B, let x = a in b(x), x(s), xL. P(x), P  Q, x:A. B(x), @i events of kind k change x to f State(ds) (val:T), x when e
Lemmas	Knd wf, secret-table wf, es-secret-server wf, nat wf, st-length wf, map wf, Id wf, event system wf, IdLnk wf, rcv wf, es-constant-1, es-E wf, es-loc wf, id-deq wf, es-kind wf, fpf-cap-single1, member map, l member wf, st-length-encrypt, es-val wf, es-vartype wf, es-when wf